Inference at * 1 0 
Iof proof for Lemma neg assert of eq int:



1. x : 
2. y : 
  (((x = y)))  x  y 

latex

 by PERMUTE{1:n, 2:n, 3:n, 3:n, 4:n, 5:n, 6:n, 7:n, 8:n, 9:n} 

latex

 1: .....wf..... NILNIL

 1:   (((x = y)))  
 2: .....wf..... NILNIL

 2:   ((x = y))  
 3: .....wf..... NILNIL

 3:   x  y  
 4: .....wf..... NILNIL

 4:   ((x = y))  
 5: .....wf..... NILNIL

 5:   (x = y)  
 6: .....wf..... NILNIL

 6:   x  
 7: .....wf..... NILNIL

 7:   y  
 8: .....wf..... NILNIL

 8:   x  y = x  y
 9: 

 9:   ((x = y))  x  y
 .

Definitions	t  T, x:A  B(x), Type, f(a), x:AB(x), , s = t, a  b  T , (i = j), b, A, , x:A. B(x), P  Q, P  Q, P  Q, P  Q
Lemmas	assert of eq int, not functionality wrt iff, iff functionality wrt iff